$\forall$$T$:Type, $L_{1}$, $L_{2}$:$T$ List, $P$, $Q$:($T$$\rightarrow\mathbb{B}$).
\\[0ex]($L_{1}$ agree\_on($T$;$a$.$P$($a$)) $L_{2}$)
\\[0ex]$\Rightarrow$ index{-}of{-}first $a$ in $L_{1}$.$P$($a$) $\wedge_{2}$ $Q$($a$) $=$ index{-}of{-}first $a$ in $L_{2}$.$P$($a$) $\wedge_{2}$ $Q$($a$) $\in$ $\mathbb{Z}$